Sorry, I told you the wrong thing here. Backs shouldn't really be "inputs" because they aren't part of the call interface — doing that would mean we need to have corresponding arguments when we generate calls to the module. I asked Shankara to add a new predicate called assume-deterministic that marks a signal as deterministic without making it part of the call interface. This probably calls for a change to declareSignals. Here's a test case Shankara and I discussed:

Input:

component Foo(reg: NondetReg) {
    Reg(r@1)
}

Expected output (probably):

(prime-number 2013265921)

(begin-module Foo)
(input reg_layout_super)
(input reg_super)
(output layout_super_super)
(output result_super_super_super)
(output result_super_reg_super)
(assume-deterministic reg_back1)
(call [layout_super_super result_super_super_super result_super_reg_super] Reg [reg_back1])
(end-module)

Looking at the full output for this test, x0 corresponds to the argument first: Val rather than the back. I think we should make a filecheck assertion about all of the inputs and signals corresponding to the back (x1_*).